PRISM

Benchmark
Model:cluster v.1 (CTMC)
Parameter(s)N = 128, T = 2000, t = 20
Property:premium_steady (steady-state-prob)
Invocation (specific)
./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 cluster.prism cluster.props --property premium_steady -const N=128,T=2000,t=20
Execution
Walltime:65.42552495002747s
Return code:0
Relative Error:1.408095131394231e-09
Log
PRISM
=====

Version: 4.5.dev
Date: Sat Mar 14 12:40:54 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 cluster.prism cluster.props --property premium_steady -const 'N=128,T=2000,t=20'

Parsing model file "cluster.prism"...

Type:        CTMC
Modules:     Left Right Repairman Line ToLeft ToRight 
Variables:   left_n left right_n right r line line_n toleft toleft_n toright toright_n 

Parsing properties file "cluster.props"...

8 properties:
(1) "below_min": R{"time_not_min"}=? [ C<=T ]
(2) "operational": R{"percent_op"}=? [ I=t ]
(3) "premium_steady": S=? [ "premium" ]
(4) "qos1": P=? [ F<=T !"minimum" ]
(5) "qos2": P=? [ F[t,t] !"minimum" ]
(6) "qos3": P=? [ "minimum" U<=t "premium" ]
(7) "qos4": P=? [ !"minimum" U>=t "minimum" ]
(8) "repairs": R{"num_repairs"}=? [ C<=T ]

---------------------------------------------------------------------

Model checking: "premium_steady": S=? [ "premium" ]
Model constants: N=128

Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).

Building model...
Model constants: N=128

Computing reachable states...

Reachability (BFS): 261 iterations in 0.18 seconds (average 0.000678, setup 0.00)

Time for model construction: 0.246 seconds.

Type:        CTMC
States:      597012 (1 initial)
Transitions: 2908192

Rate matrix: 17481 nodes (134 terminal), 2908192 minterms, vars: 25r/25c

SCCs: 1, BSCCs: 1, non-BSCC states: 0
BSCC sizes: 1:597012

Computing steady state probabilities for BSCC 1

Computing probabilities...
Engine: Sparse

Building sparse matrix... [n=597012, nnz=2908192, compact] [11.7 MB]
Creating vector for diagonals... [dist=6345, compact] [1.2 MB]
Allocating iteration vector... [4.6 MB]
TOTAL: [17.4 MB]

Starting iterations...
Iteration 390: max relative diff=0.260804, 5.01 sec so far
Iteration 780: max relative diff=0.000898, 10.02 sec so far
Iteration 1170: max relative diff=0.000138, 15.03 sec so far
Iteration 1560: max relative diff=0.000081, 20.03 sec so far
Iteration 1948: max relative diff=0.000048, 25.04 sec so far
Iteration 2338: max relative diff=0.000028, 30.04 sec so far
Iteration 2728: max relative diff=0.000016, 35.05 sec so far
Iteration 3118: max relative diff=0.000010, 40.06 sec so far
Iteration 3508: max relative diff=0.000006, 45.07 sec so far
Iteration 3897: max relative diff=0.000003, 50.07 sec so far
Iteration 4287: max relative diff=0.000002, 55.08 sec so far
Iteration 4677: max relative diff=0.000001, 60.09 sec so far

Backwards Gauss-Seidel: 4769 iterations in 63.87 seconds (average 0.012847, setup 2.60)

BSCC 1 probability: 0.9979378926049853

All states are in BSCCs (so no reachability probabilities computed)

Value in the initial state: 0.9979378926049853

Time for model checking: 64.375 seconds.

Result: 0.9979378926049853 (value in the initial state)


Overall running time: 65.255 seconds.

---------------------------------------------------------------------

Note: There was 1 warning during computation.